Symbolic trajectory evaluation (STE) is a
lattice
Lattice may refer to:
Arts and design
* Latticework, an ornamental criss-crossed framework, an arrangement of crossing laths or other thin strips of material
* Lattice (music), an organized grid model of pitch ratios
* Lattice (pastry), an ornam ...
-based
model checking
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems ...
technology that uses a form of
symbolic simulation
In computer science, a simulation is a computation of the execution of some appropriately modelled state-transition system. Typically this process models the complete state of the system at individual points in a discrete linear time frame, comp ...
. STE is essentially used for computer hardware, that is
circuit verification
Verify or verification may refer to:
General
* Verification and validation, in engineering or quality management systems, is the act of reviewing, inspecting or testing, in order to establish and document that a product, service or system meets ...
. The technique uses
abstraction, meaning that details of the circuit behaviour are removed from the circuit model. It was first developed by Carl Seger and Randy Bryant in 1995 as an alternative to "classical"
symbolic model checking.
References
* C.-J. H. Seger, and R. E. Bryant
Formal Verification by Symbolic Evaluation of Ordered Trajectories Formal Methods in System Design, Vol. 6, No. 2 (March, 1995), pp. 147–190
Model checking
Management cybernetics
{{Comp-sci-stub